$\forall$$A$, $B$:Type, $L$:(($A$$\rightarrow$($B$ + Top)) List), $x$:$A$. \\[0ex]($\uparrow$can{-}apply(p{-}first($L$);$x$)) $\Leftarrow\!\Rightarrow$ ($\exists$$f$$\in$$L$.$\uparrow$can{-}apply($f$;$x$))